(set-logic QF_UF)
(declare-sort U 0)

(declare-fun e () U)
(declare-fun f () U)
(declare-fun d () U)
(declare-fun d_p () U)

(declare-fun g_ex_1 (U) Bool)
(declare-fun g_ex_2 (U) Bool)
(declare-fun g_ex_3 (U) Bool)
(declare-fun g_ex_4 (U) Bool)
(declare-fun g_ex_5 (U) Bool)
(declare-fun g_ex_6 (U) Bool)
(declare-fun g_ex_7 (U) Bool)
(declare-fun g_ex_8 (U) Bool)
(declare-fun g_ex_9 (U) Bool)
(declare-fun g_ex_10 (U) Bool)
(declare-fun g_ex_11 (U) Bool)
(declare-fun g_ex_12 (U) Bool)
(declare-fun g_ex_13 (U) Bool)
(declare-fun g_ex_14 (U) Bool)
(declare-fun g_ex_15 (U) Bool)
(declare-fun g_ex_16 (U) Bool)
(declare-fun g_ex_17 (U) Bool)
(declare-fun g_ex_18 (U) Bool)
(declare-fun g_ex_19 (U) Bool)
(declare-fun g_ex_20 (U) Bool)
(declare-fun g_ex_21 (U) Bool)
(declare-fun g_ex_22 (U) Bool)
(declare-fun g_ex_23 (U) Bool)
(declare-fun g_ex_24 (U) Bool)
(declare-fun g_ex_25 (U) Bool)
(declare-fun g_ex_26 (U) Bool)
(declare-fun g_ex_27 (U) Bool)
(declare-fun g_ex_28 (U) Bool)
(declare-fun g_ex_29 (U) Bool)
(declare-fun g_ex_30 (U) Bool)
(declare-fun g_ex_31 (U) Bool)
(declare-fun g_ex_32 (U) Bool)

(declare-fun mul (U U) U)

(declare-fun gi (Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool Bool ) U)

(declare-fun o1 () Bool)
(declare-fun o2 () Bool)
(declare-fun o3 () Bool)
(declare-fun o4 () Bool)
(declare-fun o5 () Bool)
(declare-fun o6 () Bool)
(declare-fun o7 () Bool)
(declare-fun o8 () Bool)
(declare-fun o9 () Bool)
(declare-fun o10 () Bool)
(declare-fun o11 () Bool)
(declare-fun o12 () Bool)
(declare-fun o13 () Bool)
(declare-fun o14 () Bool)
(declare-fun o15 () Bool)
(declare-fun o16 () Bool)
(declare-fun o17 () Bool)
(declare-fun o18 () Bool)
(declare-fun o19 () Bool)
(declare-fun o20 () Bool)
(declare-fun o21 () Bool)
(declare-fun o22 () Bool)
(declare-fun o23 () Bool)
(declare-fun o24 () Bool)
(declare-fun o25 () Bool)
(declare-fun o26 () Bool)
(declare-fun o27 () Bool)
(declare-fun o28 () Bool)
(declare-fun o29 () Bool)
(declare-fun o30 () Bool)
(declare-fun o31 () Bool)
(declare-fun o32 () Bool)


(define-fun mod2 ((i1 Bool) (i2 Bool) (i3 Bool) (i4 Bool) (i5 Bool) (i6 Bool) (i7 Bool) (i8 Bool) (i9 Bool) (i10 Bool) (i11 Bool) (i12 Bool) (i13 Bool) (i14 Bool) (i15 Bool) (i16 Bool) (i17 Bool) (i18 Bool) (i19 Bool) (i20 Bool) (i21 Bool) (i22 Bool) (i23 Bool) (i24 Bool) (i25 Bool) (i26 Bool) (i27 Bool) (i28 Bool) (i29 Bool) (i30 Bool) (i31 Bool) (i32 Bool) (o1 Bool) (o2 Bool) (o3 Bool) (o4 Bool) (o5 Bool) (o6 Bool) (o7 Bool) (o8 Bool) (o9 Bool) (o10 Bool) (o11 Bool) (o12 Bool) (o13 Bool) (o14 Bool) (o15 Bool) (o16 Bool) (o17 Bool) (o18 Bool) (o19 Bool) (o20 Bool) (o21 Bool) (o22 Bool) (o23 Bool) (o24 Bool) (o25 Bool) (o26 Bool) (o27 Bool) (o28 Bool) (o29 Bool) (o30 Bool) (o31 Bool) (o32 Bool)) Bool 
(and (= i1 o1) (= o2 false) (= o3 false) (= o4 false) (= o5 false) (= o6 false) (= o7 false) (= o8 false) (= o9 false) (= o10 false) (= o11 false) (= o12 false) (= o13 false) (= o14 false) (= o15 false) (= o16 false) (= o17 false) (= o18 false) (= o19 false) (= o20 false) (= o21 false) (= o22 false) (= o23 false) (= o24 false) (= o25 false) (= o26 false) (= o27 false) (= o28 false) (= o29 false) (= o30 false) (= o31 false) (= o32 false)))
 

(assert (and 

(= (mul e  (gi o1 o2 o3 o4 o5 o6 o7 o8 o9 o10 o11 o12 o13 o14 o15 o16 o17 o18 o19 o20 o21 o22 o23 o24 o25 o26 o27 o28 o29 o30 o31 o32 )) d)

(mod2 (g_ex_1 f)(g_ex_2 f)(g_ex_3 f)(g_ex_4 f)(g_ex_5 f)(g_ex_6 f)(g_ex_7 f)(g_ex_8 f)(g_ex_9 f)(g_ex_10 f)(g_ex_11 f)(g_ex_12 f)(g_ex_13 f)(g_ex_14 f)(g_ex_15 f)(g_ex_16 f)(g_ex_17 f)(g_ex_18 f)(g_ex_19 f)(g_ex_20 f)(g_ex_21 f)(g_ex_22 f)(g_ex_23 f)(g_ex_24 f)(g_ex_25 f)(g_ex_26 f)(g_ex_27 f)(g_ex_28 f)(g_ex_29 f)(g_ex_30 f)(g_ex_31 f)(g_ex_32 f) o1 o2 o3 o4 o5 o6 o7 o8 o9 o10 o11 o12 o13 o14 o15 o16 o17 o18 o19 o20 o21 o22 o23 o24 o25 o26 o27 o28 o29 o30 o31 o32 )

(= (mul e  (gi o1 o2 o3 o4 o5 o6 o7 o8 o9 o10 o11 o12 o13 o14 o15 o16 o17 o18 o19 o20 o21 o22 o23 o24 o25 o26 o27 o28 o29 o30 o31 o32 )) d_p)
  
))
(assert (not(= d d_p) ))

(check-sat)